g:OGrp, a, b, c:|g|. (a  b)  ((c * a)  (c * b)) 

latex

Up	groups 1
Definitions	t  T, P  Q, P  Q, P & Q, x f y, P  Q, x:A. B(x), IMonoid, IGroup, True, T, , Mon, AbMon, OCMon, OGrp
Lemmas	ocgrp wf, grp car wf, grp op wf, grp leq wf, grp op preserves le, grp inv wf, inverse wf, grp id wf, monoid p wf, grp inv assoc, grp sig wf, true wf, squash wf